;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

(CL:IN-PACKAGE "STELLA")

(IN-MODULE "/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM")

(IN-DIALECT :KIF)

;------------------------------------------------------------------------------
; Basic Set Theory Definitions
;------------------------------------------------------------------------------

(ASSERT (Being Being_Empty))
(ASSERT (Being Universe))

;------------------------------------------------------------------------------
; Set Theory Function Definitions
;------------------------------------------------------------------------------

(DEFRELATION smu  ((?b1 Being) (?b2 Being) (?b3 Being)))
(DEFRELATION isc  ((?b1 Being) (?b2 Being) (?b3 Being)))
(DEFRELATION cpl  ((?b1 Being) (?b2 Being)))

;------------------------------------------------------------------------------
; Basic Relation Definitions
;------------------------------------------------------------------------------

(ASSERT (Being Being_1))
(ASSERT (Being Being_0))

(DEFRELATION sbs ((?b1 Being) (?b2 Being))) (ASSERT (closed sbs))

;------------------------------------------------------------------------------
; Subsmuption Axioms
;------------------------------------------------------------------------------

; S1-S2
(ASSERT (
	FORALL ((?x Being) (?y Being)) ( 
		<=>
			(sbs ?x ?y)
			(FORALL ((?z Being)) (
				=> (sbs ?z ?x) (sbs ?z ?y)
			))
	)
))

; S3-S4
(ASSERT (
	FORALL ((?x Being)) ( 
		AND
			(sbs ?x Being_1)
			(sbs Being_0 ?x)
	)
))

; S5
(ASSERT (
	NOT (sbs Being_1 Being_0)
))

; S6
(ASSERT (
		FORALL ((?x Being)) ( 
			=>
				(sbs Being_1 ?x)
				(FORALL ((?z Being)) (
						sbs ?z ?x
				))
		)
))

; S7
(ASSERT (
		FORALL ((?x Being)) ( 
			=>
				(sbs ?x Being_0)
				(FORALL ((?z Being)) (
						sbs ?x ?z
				))
		)
))

; Being_Empty => Being_0; Universe => Being_1
(ASSERT (
	AND 
		(sbs Being_Empty Being_0)
		(sbs Being_1 Universe)
))

;------------------------------------------------------------------------------
; Equivalence, Est and Identity Relation Axioms
;------------------------------------------------------------------------------

(DEFRELATION eqv ((?x Being) (?y Being))
:<=> 
	(AND 
			(sbs ?x ?y)
			(sbs ?y ?x)
	)
) (ASSERT (closed eqv))

(DEFRELATION est ((?x Being) (?y Being))
:<=>
	(AND 
			(sbs ?x ?y)
			(NOT (sbs ?x Being_0))
	)
) (ASSERT (closed est))

(DEFRELATION idt ((?x Being) (?y Being))
:<=>
	(AND 
			(est ?x ?y)
			(est ?y ?x)
	)
) (ASSERT (closed idt))

;------------------------------------------------------------------------------
; Set Theory ZLP Axioms
;------------------------------------------------------------------------------

; Intersection 1-2
;(ASSERT (
;	FORALL ((?x Being) (?y Being) (?z Being)) ( 
;		<=>
;			(EXISTS ((?u Being)) (
;				AND 
;					(sbs ?z ?u) (isc ?x ?y ?u)
;			))
;			(AND (sbs ?z ?x) (sbs ?z ?y))
;	)
;))
;
; Intersection 3-4
;(ASSERT (
;	FORALL ((?x Being) (?y Being) (?z Being)) ( 
;		<=>
;			(EXISTS ((?u Being)) (
;				AND 
;					(isc ?x ?y ?u) (sbs ?u ?z)
;			))
;			(FORALL ((?u Being)) (
;				=>
;					(AND (sbs ?u ?x)(sbs ?u ?y))
;					(sbs ?u ?z)
;			))		
;	)
;))
;
; Sum 1-2
;(ASSERT (
;	FORALL ((?x Being) (?y Being) (?z Being)) ( 
;		<=>
;			(sbs ?z (smu ?x ?y))
;			(EXISTS ((?u Being)) (
;				=>
;					(sbs ?u ?z)
;					(OR (sbs ?u ?x)(sbs ?u ?y))
;			))
;	)
;))
;
; Sum 3-4
;(ASSERT (
;	FORALL ((?x Being) (?y Being) (?z Being)) ( 
;		<=>
;			(sbs (smu ?x ?y) ?z)
;			(AND (sbs ?x ?z)(sbs ?y ?z))		
;	)
;))
;
; Complement 1-2
;(ASSERT (
;	FORALL ((?x Being) (?y Being)) ( 
;		<=>
;			(sbs ?x (cpl ?y))
;			(sbs (isc ?x ?y) Being_0)
;	)
;))
;
; Complement 3-4
;(ASSERT (
;	FORALL ((?x Being) (?y Being)) ( 
;		<=>
;			(sbs (cpl ?x) ?y)
;			(sbs Being_1 (smu ?x ?y))
;	)
;))
;
; Complement 5-6
;(ASSERT (
;	FORALL ((?x Being) (?y Being)) ( 
;		<=>
;			(sbs (cpl ?x) (cpl ?y))
;			(sbs ?y ?x)
;	)
;))
